\begin{tabbing}
R{-}frame{-}compat($A$;$B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=i\=f \=Reffect?($A$)$\rightarrow$\+\+\+
\\[0ex]i\=f \=Rframe?($B$)$\rightarrow$\+\+
\\[0ex]Rframe{-}x($B$) $=$ Reffect{-}x($A$) $\in$ Id $\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rframe{-}L($B$) $\in$ Knd)
\-\\[0ex]; \=Raframe?($B$)$\rightarrow$\+
\\[0ex]Raframe{-}k($B$) $=$ Reffect{-}knd($A$) $\in$ Knd $\Rightarrow$ (Reffect{-}x($A$) $\in$ Raframe{-}L($B$) $\in$ Id)
\-\\[0ex]; \=Rrframe?($B$)$\rightarrow$\+
\\[0ex]fpf{-}dom(IdDeq; Rrframe{-}x($B$); Reffect{-}ds($A$))
\\[0ex]$\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]else True fi
\-\\[0ex]; \=Rsends?($A$)$\rightarrow$\+
\\[0ex]i\=f \=Rsframe?($B$)$\rightarrow$\+\+
\\[0ex]Rsframe{-}lnk($B$) $=$ Rsends{-}l($A$) $\in$ IdLnk
\\[0ex]$\Rightarrow$ (Rsframe{-}tag($B$) $\in$ map($\lambda$$p$.1of($p$);Rsends{-}g($A$)) $\in$ Id)
\\[0ex]$\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rsframe{-}L($B$) $\in$ Knd)
\-\\[0ex]; \=Rbframe?($B$)$\rightarrow$\+
\\[0ex]Rbframe{-}k($B$) $=$ Rsends{-}knd($A$) $\in$ Knd $\Rightarrow$ (Rsends{-}l($A$) $\in$ Rbframe{-}L($B$) $\in$ IdLnk)
\-\\[0ex]; \=Rrframe?($B$)$\rightarrow$\+
\\[0ex]fpf{-}dom(IdDeq; Rrframe{-}x($B$); Rsends{-}ds($A$))
\\[0ex]$\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]else True fi
\-\\[0ex]; \=Rpre?($A$)$\rightarrow$\+
\\[0ex]if \=Rrframe?($B$)$\rightarrow$\+
\\[0ex]fpf{-}dom(IdDeq; Rrframe{-}x($B$); Rpre{-}ds($A$))
\\[0ex]$\Rightarrow$ (locl(Rpre{-}a($A$)) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\\[0ex]else True fi
\-\-\\[0ex]else True fi
\-
\end{tabbing}